Nuprl Lemma : R-and-rule 11,40
A,B:es_realizer{i:l}, P,Q:(event_system{i:l}prop{i':l}).
R-realizes{i:l}
R-realizes(A; es.P(es))
 R-realizes{i:l}
 R-realizes(B; es.Q(es))
 R-compat{i:l}
 R-compat(A; B)
 R-realizes{i:l}
 R-realizes(Rplus(A; B); es.(P(es)  Q(es))) 
latex

Definitionst  T, top, P  Q, x(s), R-realizes{i:l}(R; es.P(es)), P  Q, prop{i:l}, x:A. B(x), R-consistent(R; es)
Lemmases realizer wf, R-Feasible wf, R-compat wf, event system wf, Rplus wf, R-consistent wf, R-Feasible-Rplus

origin